(declare-fun a () (_ BitVec 1))
(declare-fun b () (_ BitVec 1))
(declare-fun c () (_ BitVec 1))
(declare-fun d () (_ BitVec 1))
(declare-fun e () (_ BitVec 1))
(declare-fun f () (_ BitVec 1))
(declare-fun g () (_ BitVec 1))
(assert (= (_ bv1 1) (bvurem (bvand (bvand (bvmul (bvand (ite (= b c) (_ bv1 1) (_ bv0 1)) (ite (= c (bvashr g d)) (_ bv1 1) (_ bv0 1))) (ite (= g e) (_ bv1 1) (_ bv0 1))) (ite (= e (bvnand f (_ bv1 1))) (_ bv1 1) (_ bv0 1))) (ite (= f (_ bv1 1)) (_ bv1 1) (_ bv0 1))) (bvnot (bvudiv (bvand b (_ bv1 1)) a)))))
(check-sat)
